Code and Notes (Week 1 Thursday)

-- btw Int is 64-bit integers
sumTo :: Int -> Int
sumTo i = if i == 0 then 0
  else sumTo (i - 1) + i


-- defining naturals Peano style

data Nat = Z | S Nat
  deriving (Show, Read)

one = S Z
two = S (S Z)

add1 :: Nat -> Nat -> Nat
add1 i Z = i
add1 i (S j) = S (add1 i j)

add2 :: Nat -> Nat -> Nat
add2 Z i = i
add2 (S i) j = S (add2 i j)



our_length :: [a] -> Int
our_length [] = 0
our_length (x : xs) = 1 + our_length xs

our_drop :: Int -> [a] -> [a]
our_drop i [] = []
our_drop i (x : xs) = if i <= 0 then (x : xs) else our_drop (i - 1) xs

our_take :: Int -> [a] -> [a]
our_take i [] = []
our_take i (x : xs) = if i <= 0 then [] else x : our_take (i - 1) xs

our_append :: [a] -> [a] -> [a]
our_append [] ys = ys
our_append (x : xs) ys = x : our_append xs ys


data Tree a = Leaf | Branch a (Tree a) (Tree a)
  deriving (Show, Read)

leaves :: Tree a -> Int
leaves Leaf = 1
leaves (Branch x l r) = leaves l + leaves r

height :: Tree a -> Int
height Leaf = 1
height (Branch x l r) = max (height l) (height r) + 1

example_tree = Branch 12 Leaf (Branch 5 Leaf Leaf)



data Forest a = Empty | Cons (Rose a) (Forest a)
  deriving (Show, Read)

data Rose a = Node a (Forest a)
  deriving (Show, Read)


height_rose :: Rose a -> Int
height_rose (Node _ forest) = height_forest forest + 1

height_forest :: Forest a -> Int
height_forest Empty = 0
height_forest (Cons r f) = max (height_rose r) (height_forest f)

Prove ∀n. sumTo n = (n * (n + 1)) / 2

By induction (on n). P (n) ⇔ sumTo n = (n * (n + 1)) / 2

BTW we could say P ⇔ λn. sumTo n = (n * (n + 1)) / 2

Prove P (0): sumTo 0 = (0 * (0 + 1)) / 2
   = (if 0 = 0 then 0 else ...) = ...

Inductive case. Assume P (i):
    sumTo i = (i * (i + 1)) / 2

Show P (i + 1):
    sumTo (i + 1) = ((i + 1) * ((i + 1) + 1)) / 2

Equivalent to:
   if i + 1 = 0 then 0 else sumTo ((i + 1) - 1) + (i + 1) = rhs
Equivalent to:
   sumTo i + (i + 1) = rhs
Use IH:
    ((i * (i + 1)) / 2) + (i + 1) = rhs

Prove ∀n. add2 n Z = n
Using induction with P (n) = (add2 n Z = n)

Base case P (Z) :
  add2 Z Z = Z by definition

Inductive case (S i) :

Assume add2 i Z = i
Show add2 (S i) Z = S i

We have add2 (S i) Z
  = S (add2 i Z)                -- by definition of add2
  = S i                         -- by IH
  QED.

Prove ∀xs. our_take (length xs) xs = xs

By induction on the shape of xs using P(xs) = our_take (length xs) xs = xs

Base case P []:
  our_take (length []) [] = []  -- by definition of our_take

Inductive case P (x : xs):
  assuming our_take (length xs) xs = xs


  our_take (length (x : xs)) (x : xs) = xs

  lhs
  = our_take (length xs + 1) (x : xs)
                        -- by definition of length
  = if length xs + 1 <= 0 then [] else x : our_take (length xs + 1) - 1) xs
                        -- by definition of our_take
  = x : our_take (length xs) xs
                        -- as length non-negative
  = x : xs              -- by IH
  QED.

Prove ∀xs.
  our_take 5 xs ++ our_drop 5 xs = xs

First prove ∀xs. ∀n.
  our_take n xs ++ our_drop n xs = xs



By induction on the shape of xs


P ⇔ λxs. ∀n. our_take n xs ++ our_drop n xs = xs

Base Case:
  ∀n. our_take n [] ++ our_drop n [] = []

For any n, this follows from the definitions.


Inductive Case:

Assume 
  ∀n. our_take n xs ++ our_drop n xs = xs
Show
  ∀n. our_take n (x : xs) ++ our_drop n (x : xs) = (x : xs)

Fix n.

By definitions, this is equivalent to

  (if n <= 0 then [] else x : our_take (n - 1) xs) ++
  (if n <= 0 then (x : xs) else our_drop (n - 1) xs) = (x : xs)

Take cases on n <= 0.

If it is, our goal is equivalent to

  [] ++ (x : xs) = (x : xs)

  which follows from the definition of append.

If not, equivalent to

  (x : our_take (n - 1) xs) ++ (our_drop (n - 1) xs) = (x : xs)

  which in turn (thanks to definition of append) is equivalent to

  x : (our_take (n - 1) xs ++ our_drop (n - 1) xs) = (x : xs)

  which follows from IH (with n specialised to n - 1).

Prove ∀t. height t ≤ leaves t

By induction on the shape of t

Base case
   height Leaf ≤ leaves Leaf
   By definitions

Recursive case, assume
   height l ≤ leaves l
   height r ≤ leaves r

Prove:
   height (Branch x l r) ≤ leaves (Branch x l r)

Equivalent to:
   max (height l + 1) (height r + 1) ≤ leaves l + leaves r

This follows from two things. Firstly, a case division on whether
l or r has greater height (i.e. how max is calculated). Secondly,
we need to establish that ∀t. leaves t ≥ 1, either as a separate
lemma or by adding it to our inductive statement.